mcsta/modest mcsta crowds.jani -E TotalRuns=6,CrowdSize=20 --props positive -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 5e-2 --width 5e-2 --relative-width --p0 --p1
crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 40 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 10291282 states for TotalRuns=6, CrowdSize=20.
Peak memory usage: 3438 MB
Analysis results for crowds.jani
Experiment TotalRuns=6, CrowdSize=20
+ State space exploration
State size: 40 bytes
States: 10291282
Transitions: 10291282
Branches: 37068802
Rate: 395895 states/s
Time: 27.3 s
+ Property positive
Probability: 0.12239151218950753
Bounds: [0.11947382041613554, 0.1253092039628795]
Time: 6.6 s
+ Precomputations
Min. prob. 0 states: 8587502
Time for min. prob. 0 states: 2.5 s
Min. prob. 1 states: 21252
Time for min. prob. 1 states: 0.4 s
+ Essential states
Iterations: 2
Essential states: 1275122
Transitions: 1275122
Branches: 10200962
Time: 1.3 s
+ Optimistic value iteration
Total iterations: 29
Verif. attempts: 2
Verif. iterations: 9
Final epsilon: 0.013026946067679426
Time: 2.5 s
Exported results to file "/out.txt".